package test;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Set;

import util.Pair;
import util.Timer;

import dd.discrete.ADD;
import dd.discrete.ADDDNode;
import dd.discrete.ADDINode;
import dd.discrete.ADDNode;
import dd.discrete.DD;

public class constraintRestrict implements Runnable{

	private int g;
	private int f;
	private ADD context;

	public constraintRestrict(ADD context, int f, int g) {
		this.context = context;
		this.f = f;
		this.g = g;
	}
	

	public static void main(String[] args) {
		
		final int nVarsMax = 15;
		final int nTrials = 20;
		
		for( int i = 5; i <= nVarsMax ; ++i ){
			for( int j = 0 ; j < nTrials ; ++j ){
				
				Pair<ADD, ArrayList<String> > pair = makeContext(i);
				ADD context = pair._o1;
				
				double fdensity = Math.random();
				double gdensity = Math.random();

				List<String> order = pair._o2.subList(0, i);
				
				int f = makeRandomADD(context,  order, fdensity, false);
				int g = makeRandomADD(context, order, gdensity, true);
				
				constraintRestrict CR = new constraintRestrict(context, f, g);
				Thread worker = new Thread(CR, i+ " " + fdensity + " " + gdensity );
				worker.start();
			}		
		}
	}

	private Pair<Boolean, Pair<Long, Double>> checkConstraint(ADD context, int ret) {
		
		boolean pass = checkConstraintInt(context, g, ret);
		
		if( ! pass ){
			System.err.println("err");
			System.exit(1);
		}
		
		Timer oldTimer = new Timer();
		int oldd = context.applyInt(f, g, DD.ARITH_PROD);
		double oldt = oldTimer.GetTimeSoFarAndResetInMinutes();
		
		return new Pair<Boolean, Pair<Long, Double>>(pass, 
				new Pair<Long, Double>(context.countExactNodes(oldd), oldt));
		
	}

	private boolean checkConstraintInt(ADD context, final int con, int ret) {
		
		ADDNode node = context.getNode(ret);
		if( node instanceof ADDDNode && con == context.getConstantNode(0.0d) 
				&& ((ADDDNode)node)._dUpper == context.NEGINF ){
			return true;			
		}else if( node instanceof ADDDNode && con != context.getConstantNode(0.0d)  
				&& ((ADDDNode)node)._dUpper != context.NEGINF ){
			return true;
		}else if( node instanceof ADDINode ){
			ADDINode inode = (ADDINode)node;
			boolean truecheck = checkConstraintInt(context, 
					context.restrict(con, inode._nTestVarID, DD.RESTRICT_HIGH),
					inode._nHigh);
			if( ! truecheck ){
				return false;
			}
			boolean falsecheck = checkConstraintInt(context,  
					context.restrict(con, inode._nTestVarID, DD.RESTRICT_LOW),
					inode._nLow);
			return falsecheck;
		}
		
		return false;
	}

	private int numberOfDisjointVars(ADD context, int f, int g) {
		Set thing = context.getGIDs(g);
		thing.removeAll( context.getGIDs(f) );
		return thing.size();
	}

	private static int makeRandomADD(ADD context, List<String> order, final double density, 
			final boolean BDD) {
		//pick random variable
		//recurse
		//at leaf get random double
		return makeRandomADDInt(context, order, density, 0, BDD);
	}

	private static int makeRandomADDInt(ADD context, List<String> vars, 
			final double density, int index, final boolean BDD) {
		if( index == vars.size() ){
			return context.getConstantNode(BDD ? (Math.random() < 0.5 ? 0.0 : 1.0) : Math.random());
		}
		
		if( Math.random() < density ){
			int high = makeRandomADDInt(context, vars, density, index+1, BDD);
			int low = makeRandomADDInt(context, vars, density, index+1, BDD);
			
			int id = (Integer)context._hmVarName2ID.get(vars.get(index));
			
			int lowbr = context.getVarNode(id, 1.0d, 0.0d);
			
			int highbr = context.getVarNode(id, 0.0d, 1.0d);

			low = context.applyInt(low, lowbr, DD.ARITH_PROD );
			high = context.applyInt(high, highbr, DD.ARITH_PROD );
			
			return context.applyInt(low, high, DD.ARITH_SUM );
		}
		return makeRandomADDInt(context, vars, density, index+1, BDD);
	}

	private static Pair<ADD, ArrayList<String> > makeContext(int i) {
		ArrayList<String> order = new ArrayList<String>();
		
		for( int j = 0 ; j < i; ++j ){
			order.add(String.valueOf((char)('A'+j)));
		}
		
		return new Pair<ADD, ArrayList<String> >( new ADD(order), order );
		
	}

	@Override
	public void run() {
		// int disjoint = numberOfDisjointVars(context, f,g);
		Timer conTime = new Timer();
		int ret = context.constrainRestrict(f, g);
		double t = conTime.GetTimeSoFarAndResetInMinutes();
		context.addSpecialNode(f);
		context.addSpecialNode(g);
		context.addSpecialNode(ret);
		context.flushCaches(false);
		Pair<Boolean, Pair<Long, Double>> passed = checkConstraint(context,ret);
		if( !passed._o1 ){
			System.err.println("fail");
			System.exit(1);
		}
		
		int disjoint = numberOfDisjointVars(context, f, g);
		System.out.println(disjoint
				+ " " + context.countExactNodes(f) 
				+ " " + context.countExactNodes(g) 
				+ " " + context.countExactNodes(ret)
				+ " " + passed._o2._o1
				+ " " + t + " " + passed._o2._o2 );
		
		context.clearSpecialNodes();
		context.flushCaches(false);
	}
	
}
